T:Type, eq:EqDecider(T), es:ES, x:Id, e:{e:E| @loc(e)(x:T)} , e':E.
(((e' <loc e) & (((x when e') = (x when e)  T)) & e''[e',e).(x after e'') = (x when e)  T)
 (e' = e & (e''<e. (x after e'') = (x when e'')  T)))
 (lastchange(x;e) = e') 

latex

Definitions

e loc e' , x:A. B(x), A, True, T, @i(x:T), ff, tt, if b then t else f fi , P  Q, P  Q, x. t(x), , t  T, A c B, lastchange(x;e), (e <loc e'), P & Q, P  Q, P  Q, EqDecider(T), x:A. B(x), e<e'.P(e), e<e'. P(e), e(e1,e2].P(e), {T}, SQType(T), False, e[e1,e2).P(e), SqStable(P), Unit, , x(s),

Lemmas

assert-changed, es-le-loc, has-changed, Id sq, alle-between1-after-1, es-le weakening, es-le weakening eq, es-locl wf, sq stable subtype rel, decidable assert, es-isconst wf, sq stable from decidable, last-change-equal, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bnot wf, changed wf, assert wf, iff wf, bool wf, event system wf, es-dtype wf, es-E wf, alle-lt wf, es-locl-iff, es-loc-pred, es-after wf, alle-between1 wf, es-vartype wf, es-when wf, not wf, es-causl wf, es-loc wf, Id wf